$\forall$$T$:Type, $P$:($L$:($T$ List)$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel-$1}}$$\rightarrow$Prop).
\\[0ex]guarded\_permutation($T$;$P$) $\in$ ($T$ List)$\rightarrow$($T$ List)$\rightarrow$Prop